1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114

use crate::sketchbook::observations::{Observation, VarValue};
use biodivine_lib_param_bn::biodivine_std::traits::Set;
use biodivine_lib_param_bn::symbolic_async_graph::{GraphColors, SymbolicAsyncGraph};
use biodivine_lib_param_bn::trap_spaces::{NetworkColoredSpaces, SymbolicSpaceContext, TrapSpaces};
use biodivine_lib_param_bn::ExtendedBoolean;
use biodivine_lib_param_bn::Space;

/// Wrapper to compute all essential colored trap spaces (under an optional set restriction).
pub fn compute_essential_trap_spaces(
    graph: &SymbolicAsyncGraph,
    ctx: &SymbolicSpaceContext,
    restriction: Option<NetworkColoredSpaces>,
) -> NetworkColoredSpaces {
    let unit_set = if let Some(restrict_set) = restriction {
        restrict_set
    } else {
        ctx.mk_unit_colored_spaces(graph)
    };

    TrapSpaces::essential_symbolic(ctx, graph, &unit_set)
}

/// Compute colors where each given observation corresponds to essential trap spaces.
pub fn colors_where_essential_traps(
    observations: Vec<Observation>,
    var_names: &[String],
    graph: &SymbolicAsyncGraph,
    ctx: &SymbolicSpaceContext,
) -> GraphColors {
    // TODO: before computing Essential traps, restrict the colors to only the ones where all observations are trap spaces

    // compute essential spaces
    let essential_traps = compute_essential_trap_spaces(graph, ctx, None);

    // one-by-one, get colors where all observation spaces are essential traps
    let mut sat_colors = essential_traps.colors();
    for observation in observations {
        let obs_space_singleton: NetworkColoredSpaces =
            encode_obs_as_singleton_space(observation, var_names, graph, ctx);
        let intersection = essential_traps.intersect(&obs_space_singleton);
        sat_colors = sat_colors.intersect(&intersection.colors());
    }
    sat_colors
}

/// Wrapper to compute all minimal colored trap spaces (under an optional set restriction).
pub fn compute_minimal_trap_spaces(
    graph: &SymbolicAsyncGraph,
    ctx: &SymbolicSpaceContext,
    restriction: Option<NetworkColoredSpaces>,
) -> NetworkColoredSpaces {
    let unit_set = if let Some(restrict_set) = restriction {
        restrict_set
    } else {
        ctx.mk_unit_colored_spaces(graph)
    };

    TrapSpaces::minimal_symbolic(ctx, graph, &unit_set)
}

/// Compute colors where each given observation corresponds to minimal trap spaces.
pub fn colors_where_minimal_traps(
    observations: Vec<Observation>,
    var_names: &[String],
    graph: &SymbolicAsyncGraph,
    ctx: &SymbolicSpaceContext,
) -> GraphColors {
    // TODO: before computing Minimal traps, restrict the colors to only the ones where all observations are trap spaces
    // TODO: maybe also restrict the colors to only the ones where the observations are essential trap spaces

    // compute minimal spaces
    let minimal_traps = compute_minimal_trap_spaces(graph, ctx, None);

    // one-by-one, get colors where all observation spaces are minimal traps
    let mut sat_colors = minimal_traps.colors();
    for observation in observations {
        let obs_space_singleton: NetworkColoredSpaces =
            encode_obs_as_singleton_space(observation, var_names, graph, ctx);
        let intersection = minimal_traps.intersect(&obs_space_singleton);
        sat_colors = sat_colors.intersect(&intersection.colors());
    }
    sat_colors
}

/// Utility to encode observation as a singleton "NetworkColoredSpaces" instance,
/// i.e., a singleton space with all the colors.
fn encode_obs_as_singleton_space(
    observation: Observation,
    var_names: &[String],
    graph: &SymbolicAsyncGraph,
    ctx: &SymbolicSpaceContext,
) -> NetworkColoredSpaces {
    let bn = graph.as_network().unwrap();

    // encode the observation into Space instance
    let mut obs_space = Space::new(bn);
    var_names.iter().enumerate().for_each(|(i, var_name)| {
        let var = bn.as_graph().find_variable(var_name).unwrap();

        match observation.get_values()[i] {
            VarValue::True => {
                obs_space[var] = ExtendedBoolean::One;
            }
            VarValue::False => {
                obs_space[var] = ExtendedBoolean::Zero;
            }
            VarValue::Any => {}
        }
    });

    // compute BDD for the space, so we can create "NetworkColoredSpaces" instance
    let obs_space_bdd = ctx.mk_space(&obs_space);
    NetworkColoredSpaces::new(obs_space_bdd, ctx)
}